$\forall$$T$:Type, $t$:$T$, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$($T$ + Top)).
\\[0ex]Normal(${\it ds}$) $\Rightarrow$ (weakSendDoApplyR\{a:ut2, tg:ut2\}($T$; $t$; $l$; ${\it ds}$; $f$) $\in$ Realizer)